Runtime Complexity (innermost) proof of /tmp/tmp3b2-ND/MYNAT

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^3)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))

↳2 CdtProblem

↳3 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))

↳4 CdtProblem

↳5 CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID))

↳6 CdtProblem

↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

↳8 CdtProblem

↳9 CdtKnowledgeProof (⇔)

↳10 CdtProblem

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳12 CdtProblem

↳13 CdtKnowledgeProof (⇔)

↳14 CdtProblem

↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

↳16 CdtProblem

↳17 CdtKnowledgeProof (⇔)

↳18 CdtProblem

↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))

↳20 CdtProblem

↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))

↳22 CdtProblem

↳23 CdtKnowledgeProof (⇔)

↳24 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

U11(tt, V1, V2) → U12(isNatKind(V1), V1, V2)
U12(tt, V1, V2) → U13(isNatKind(V2), V1, V2)
U13(tt, V1, V2) → U14(isNatKind(V2), V1, V2)
U14(tt, V1, V2) → U15(isNat(V1), V2)
U15(tt, V2) → U16(isNat(V2))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(V1), V1)
U22(tt, V1) → U23(isNat(V1))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(V2))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(N), N)
U52(tt, N) → N
U61(tt, M, N) → U62(isNatKind(M), M, N)
U62(tt, M, N) → U63(isNat(N), M, N)
U63(tt, M, N) → U64(isNatKind(N), M, N)
U64(tt, M, N) → s(plus(N, M))
isNat(0) → tt
isNat(plus(V1, V2)) → U11(isNatKind(V1), V1, V2)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatKind(0) → tt
isNatKind(plus(V1, V2)) → U31(isNatKind(V1), V2)
isNatKind(s(V1)) → U41(isNatKind(V1))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(isNat(M), M, N)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U15'(tt, z0) → c4(U16'(isNat(z0)), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(U23'(isNat(z0)), ISNAT(z0))
U31'(tt, z0) → c9(U32'(isNatKind(z0)), ISNATKIND(z0))
U51'(tt, z0) → c12(U52'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(U41'(isNatKind(z0)), ISNATKIND(z0))
PLUS(z0, 0) → c24(U51'(isNat(z0), z0), ISNAT(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))

S tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U15'(tt, z0) → c4(U16'(isNat(z0)), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(U23'(isNat(z0)), ISNAT(z0))
U31'(tt, z0) → c9(U32'(isNatKind(z0)), ISNATKIND(z0))
U51'(tt, z0) → c12(U52'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(U41'(isNatKind(z0)), ISNATKIND(z0))
PLUS(z0, 0) → c24(U51'(isNat(z0), z0), ISNAT(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))

K tuples:none
Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U15', U21', U22', U31', U51', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS

Compound Symbols:

c, c1, c2, c3, c4, c6, c7, c9, c12, c14, c15, c16, c17, c19, c20, c22, c23, c24, c25

(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U15'(tt, z0) → c4(U16'(isNat(z0)), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(U23'(isNat(z0)), ISNAT(z0))
U31'(tt, z0) → c9(U32'(isNatKind(z0)), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(U41'(isNatKind(z0)), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(U52'(isNatKind(z0), z0))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))

S tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U15'(tt, z0) → c4(U16'(isNat(z0)), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(U23'(isNat(z0)), ISNAT(z0))
U31'(tt, z0) → c9(U32'(isNatKind(z0)), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(U41'(isNatKind(z0)), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(U52'(isNatKind(z0), z0))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))

K tuples:none
Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U15', U21', U22', U31', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51'

Compound Symbols:

c, c1, c2, c3, c4, c6, c7, c9, c14, c15, c16, c17, c19, c20, c22, c23, c25, c5

(5) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

S tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

K tuples:none
Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U21', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51', U15', U22', U31'

Compound Symbols:

c, c1, c2, c3, c6, c14, c15, c16, c17, c19, c20, c22, c25, c5, c4, c7, c9, c23, c5

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))

We considered the (Usable) Rules:

isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U41(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt

And the Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(ISNAT(x₁)) = 0
POL(ISNATKIND(x₁)) = 0
POL(PLUS(x₁, x₂)) = [4]x₁ + x₂
POL(U11(x₁, x₂, x₃)) = [2] + [4]x₁ + [3]x₂ + [2]x₃
POL(U11'(x₁, x₂, x₃)) = 0
POL(U12(x₁, x₂, x₃)) = [5] + [3]x₂ + [5]x₃
POL(U12'(x₁, x₂, x₃)) = 0
POL(U13(x₁, x₂, x₃)) = [5] + [2]x₁ + [3]x₂ + [5]x₃
POL(U13'(x₁, x₂, x₃)) = 0
POL(U14(x₁, x₂, x₃)) = [2] + [3]x₁ + [3]x₂ + [3]x₃
POL(U14'(x₁, x₂, x₃)) = 0
POL(U15(x₁, x₂)) = [2] + [3]x₁ + [3]x₂
POL(U15'(x₁, x₂)) = 0
POL(U16(x₁)) = [2] + [2]x₁
POL(U21(x₁, x₂)) = [5] + [2]x₁ + [2]x₂
POL(U21'(x₁, x₂)) = 0
POL(U22(x₁, x₂)) = [3] + [2]x₁ + [5]x₂
POL(U22'(x₁, x₂)) = 0
POL(U23(x₁)) = [3] + [4]x₁
POL(U31(x₁, x₂)) = [4]x₁ + [2]x₂
POL(U31'(x₁, x₂)) = 0
POL(U32(x₁)) = [2] + [2]x₁
POL(U41(x₁)) = [3] + [2]x₁
POL(U51'(x₁, x₂)) = [4]x₂
POL(U61'(x₁, x₂, x₃)) = [4] + x₂ + [4]x₃
POL(U62'(x₁, x₂, x₃)) = [2] + x₂ + [4]x₃
POL(U63'(x₁, x₂, x₃)) = x₂ + [4]x₃
POL(U64'(x₁, x₂, x₃)) = x₂ + [4]x₃
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c22(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5) = 0
POL(c5(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(isNat(x₁)) = [2]
POL(isNatKind(x₁)) = 0
POL(plus(x₁, x₂)) = [2] + [3]x₂
POL(s(x₁)) = [4] + x₁
POL(tt) = 0

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

S tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

K tuples:

U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))

Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U21', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51', U15', U22', U31'

Compound Symbols:

c, c1, c2, c3, c6, c14, c15, c16, c17, c19, c20, c22, c25, c5, c4, c7, c9, c23, c5

(9) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U51'(tt, z0) → c5
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U51'(tt, z0) → c5(ISNATKIND(z0))
U51'(tt, z0) → c5

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

S tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))

K tuples:

U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U51'(tt, z0) → c5
U51'(tt, z0) → c5(ISNATKIND(z0))

Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U21', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51', U15', U22', U31'

Compound Symbols:

c, c1, c2, c3, c6, c14, c15, c16, c17, c19, c20, c22, c25, c5, c4, c7, c9, c23, c5

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))

We considered the (Usable) Rules:

isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U41(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt

And the Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]
POL(ISNAT(x₁)) = x₁
POL(ISNATKIND(x₁)) = 0
POL(PLUS(x₁, x₂)) = [1] + x₂² + [2]x₁·x₂ + x₁²
POL(U11(x₁, x₂, x₃)) = 0
POL(U11'(x₁, x₂, x₃)) = x₂ + [2]x₃ + [2]x₃² + x₂²
POL(U12(x₁, x₂, x₃)) = 0
POL(U12'(x₁, x₂, x₃)) = x₂ + [2]x₃ + x₂²
POL(U13(x₁, x₂, x₃)) = 0
POL(U13'(x₁, x₂, x₃)) = x₂ + [2]x₃ + x₂²
POL(U14(x₁, x₂, x₃)) = 0
POL(U14'(x₁, x₂, x₃)) = x₂ + [2]x₃ + x₂²
POL(U15(x₁, x₂)) = 0
POL(U15'(x₁, x₂)) = x₂
POL(U16(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21'(x₁, x₂)) = x₂
POL(U22(x₁, x₂)) = 0
POL(U22'(x₁, x₂)) = x₂
POL(U23(x₁)) = 0
POL(U31(x₁, x₂)) = 0
POL(U31'(x₁, x₂)) = 0
POL(U32(x₁)) = 0
POL(U41(x₁)) = 0
POL(U51'(x₁, x₂)) = x₂²
POL(U61'(x₁, x₂, x₃)) = [2] + x₃ + x₃² + [2]x₂·x₃ + x₂²
POL(U62'(x₁, x₂, x₃)) = [1] + x₃ + x₃² + [2]x₂·x₃ + x₂²
POL(U63'(x₁, x₂, x₃)) = [1] + x₃² + [2]x₂·x₃ + x₂²
POL(U64'(x₁, x₂, x₃)) = [1] + x₃² + [2]x₂·x₃ + x₂²
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c22(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5) = 0
POL(c5(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(isNat(x₁)) = 0
POL(isNatKind(x₁)) = 0
POL(plus(x₁, x₂)) = [2]x₁ + [2]x₂ + [3]x₂² + x₁²
POL(s(x₁)) = [1] + x₁
POL(tt) = 0

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

S tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))

K tuples:

U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U51'(tt, z0) → c5
U51'(tt, z0) → c5(ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))

Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U21', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51', U15', U22', U31'

Compound Symbols:

c, c1, c2, c3, c6, c14, c15, c16, c17, c19, c20, c22, c25, c5, c4, c7, c9, c23, c5

(13) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

S tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))

K tuples:

U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U51'(tt, z0) → c5
U51'(tt, z0) → c5(ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(ISNAT(z0))

Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U21', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51', U15', U22', U31'

Compound Symbols:

c, c1, c2, c3, c6, c14, c15, c16, c17, c19, c20, c22, c25, c5, c4, c7, c9, c23, c5

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))

We considered the (Usable) Rules:

isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U41(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt

And the Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(ISNAT(x₁)) = x₁
POL(ISNATKIND(x₁)) = 0
POL(PLUS(x₁, x₂)) = [1] + x₂² + x₁·x₂
POL(U11(x₁, x₂, x₃)) = 0
POL(U11'(x₁, x₂, x₃)) = [1] + [2]x₂ + [2]x₃ + x₂·x₃
POL(U12(x₁, x₂, x₃)) = 0
POL(U12'(x₁, x₂, x₃)) = x₂ + [2]x₃ + x₂·x₃
POL(U13(x₁, x₂, x₃)) = 0
POL(U13'(x₁, x₂, x₃)) = x₂ + x₃
POL(U14(x₁, x₂, x₃)) = 0
POL(U14'(x₁, x₂, x₃)) = x₂ + x₃
POL(U15(x₁, x₂)) = 0
POL(U15'(x₁, x₂)) = x₂
POL(U16(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21'(x₁, x₂)) = x₂
POL(U22(x₁, x₂)) = 0
POL(U22'(x₁, x₂)) = x₂
POL(U23(x₁)) = 0
POL(U31(x₁, x₂)) = 0
POL(U31'(x₁, x₂)) = 0
POL(U32(x₁)) = 0
POL(U41(x₁)) = 0
POL(U51'(x₁, x₂)) = [1] + x₂
POL(U61'(x₁, x₂, x₃)) = [2] + x₃ + x₂·x₃ + x₂²
POL(U62'(x₁, x₂, x₃)) = [2] + x₃ + x₂·x₃ + x₂²
POL(U63'(x₁, x₂, x₃)) = [2] + x₂·x₃ + x₂²
POL(U64'(x₁, x₂, x₃)) = [2] + x₂·x₃ + x₂²
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c22(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5) = 0
POL(c5(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(isNat(x₁)) = 0
POL(isNatKind(x₁)) = 0
POL(plus(x₁, x₂)) = [2] + [2]x₁ + [2]x₂ + x₁·x₂
POL(s(x₁)) = [1] + x₁
POL(tt) = 0

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

S tuples:

U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))

K tuples:

U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U51'(tt, z0) → c5
U51'(tt, z0) → c5(ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))

Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U21', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51', U15', U22', U31'

Compound Symbols:

c, c1, c2, c3, c6, c14, c15, c16, c17, c19, c20, c22, c25, c5, c4, c7, c9, c23, c5

(17) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
U15'(tt, z0) → c4(ISNAT(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

S tuples:

ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))

K tuples:

U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U51'(tt, z0) → c5
U51'(tt, z0) → c5(ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))

Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U21', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51', U15', U22', U31'

Compound Symbols:

c, c1, c2, c3, c6, c14, c15, c16, c17, c19, c20, c22, c25, c5, c4, c7, c9, c23, c5

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ISNATKIND(s(z0)) → c23(ISNATKIND(z0))

We considered the (Usable) Rules:

isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U41(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt

And the Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(ISNAT(x₁)) = x₁²
POL(ISNATKIND(x₁)) = x₁
POL(PLUS(x₁, x₂)) = x₁²·x₂ + x₁·x₂² + x₂³
POL(U11(x₁, x₂, x₃)) = 0
POL(U11'(x₁, x₂, x₃)) = [1] + x₂ + x₃ + x₃² + x₂³ + x₁·x₂² + x₂·x₃² + x₁·x₂·x₃ + x₁²·x₂ + x₁³ + x₃³
POL(U12(x₁, x₂, x₃)) = 0
POL(U12'(x₁, x₂, x₃)) = x₂ + x₃ + x₃² + x₂·x₃ + x₂² + x₂³ + x₃³
POL(U13(x₁, x₂, x₃)) = 0
POL(U13'(x₁, x₂, x₃)) = x₂ + x₃² + x₂·x₃ + x₁·x₃ + x₂² + x₂³
POL(U14(x₁, x₂, x₃)) = 0
POL(U14'(x₁, x₂, x₃)) = x₂ + x₃² + x₂·x₃ + x₂² + x₂³
POL(U15(x₁, x₂)) = 0
POL(U15'(x₁, x₂)) = x₂²
POL(U16(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21'(x₁, x₂)) = x₂ + x₂²
POL(U22(x₁, x₂)) = 0
POL(U22'(x₁, x₂)) = x₂²
POL(U23(x₁)) = 0
POL(U31(x₁, x₂)) = [1] + x₁²·x₂ + x₁·x₂² + x₂³
POL(U31'(x₁, x₂)) = x₂ + x₂²
POL(U32(x₁)) = [1] + x₁
POL(U41(x₁)) = x₁
POL(U51'(x₁, x₂)) = [1] + x₂
POL(U61'(x₁, x₂, x₃)) = x₂ + x₃ + x₃² + x₂·x₃ + x₂² + x₂³ + x₂²·x₃ + x₂·x₃²
POL(U62'(x₁, x₂, x₃)) = x₃ + x₃² + x₂·x₃ + x₂³ + x₂²·x₃ + x₂·x₃²
POL(U63'(x₁, x₂, x₃)) = x₃ + x₂·x₃ + x₂³ + x₂²·x₃ + x₂·x₃²
POL(U64'(x₁, x₂, x₃)) = x₂·x₃ + x₂³ + x₂²·x₃ + x₂·x₃²
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c22(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5) = 0
POL(c5(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(isNat(x₁)) = 0
POL(isNatKind(x₁)) = x₁²
POL(plus(x₁, x₂)) = [1] + x₁ + x₂ + x₂² + x₁·x₂ + x₁² + x₁³ + x₁·x₂²
POL(s(x₁)) = [1] + x₁
POL(tt) = [1]

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

S tuples:

ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))

K tuples:

U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U51'(tt, z0) → c5
U51'(tt, z0) → c5(ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))

Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U21', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51', U15', U22', U31'

Compound Symbols:

c, c1, c2, c3, c6, c14, c15, c16, c17, c19, c20, c22, c25, c5, c4, c7, c9, c23, c5

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))

We considered the (Usable) Rules:

isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U41(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt

And the Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]
POL(ISNAT(x₁)) = x₁²
POL(ISNATKIND(x₁)) = x₁
POL(PLUS(x₁, x₂)) = x₁·x₂ + x₁²·x₂ + x₂³
POL(U11(x₁, x₂, x₃)) = 0
POL(U11'(x₁, x₂, x₃)) = [1] + x₂ + x₃ + x₃² + x₂·x₃ + x₂² + x₂²·x₃ + x₁·x₂·x₃ + x₃³
POL(U12(x₁, x₂, x₃)) = 0
POL(U12'(x₁, x₂, x₃)) = x₃ + x₃² + x₂² + x₃³
POL(U13(x₁, x₂, x₃)) = 0
POL(U13'(x₁, x₂, x₃)) = x₃² + x₁·x₃ + x₂²
POL(U14(x₁, x₂, x₃)) = 0
POL(U14'(x₁, x₂, x₃)) = x₃² + x₂²
POL(U15(x₁, x₂)) = 0
POL(U15'(x₁, x₂)) = x₂²
POL(U16(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21'(x₁, x₂)) = x₂ + x₂²
POL(U22(x₁, x₂)) = 0
POL(U22'(x₁, x₂)) = x₂²
POL(U23(x₁)) = 0
POL(U31(x₁, x₂)) = x₁ + x₂ + x₁·x₂² + x₂³
POL(U31'(x₁, x₂)) = x₂ + x₂²
POL(U32(x₁)) = [1] + x₁
POL(U41(x₁)) = [1]
POL(U51'(x₁, x₂)) = x₂
POL(U61'(x₁, x₂, x₃)) = x₂ + x₃ + x₃² + x₂·x₃ + x₂² + x₂³ + x₂·x₃²
POL(U62'(x₁, x₂, x₃)) = x₃ + x₃² + x₂·x₃ + x₂³ + x₂·x₃²
POL(U63'(x₁, x₂, x₃)) = x₃ + x₂·x₃ + x₂³ + x₂·x₃²
POL(U64'(x₁, x₂, x₃)) = x₂·x₃ + x₂³ + x₂·x₃²
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c15(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c20(x₁, x₂)) = x₁ + x₂
POL(c22(x₁, x₂)) = x₁ + x₂
POL(c23(x₁)) = x₁
POL(c25(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5) = 0
POL(c5(x₁)) = x₁
POL(c6(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(isNat(x₁)) = 0
POL(isNatKind(x₁)) = x₁²
POL(plus(x₁, x₂)) = [1] + x₁ + x₂ + x₂² + x₁·x₂ + x₁²·x₂
POL(s(x₁)) = [1] + x₁
POL(tt) = [1]

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

U11(tt, z0, z1) → U12(isNatKind(z0), z0, z1)
U12(tt, z0, z1) → U13(isNatKind(z1), z0, z1)
U13(tt, z0, z1) → U14(isNatKind(z1), z0, z1)
U14(tt, z0, z1) → U15(isNat(z0), z1)
U15(tt, z0) → U16(isNat(z0))
U16(tt) → tt
U21(tt, z0) → U22(isNatKind(z0), z0)
U22(tt, z0) → U23(isNat(z0))
U23(tt) → tt
U31(tt, z0) → U32(isNatKind(z0))
U32(tt) → tt
U41(tt) → tt
U51(tt, z0) → U52(isNatKind(z0), z0)
U52(tt, z0) → z0
U61(tt, z0, z1) → U62(isNatKind(z0), z0, z1)
U62(tt, z0, z1) → U63(isNat(z1), z0, z1)
U63(tt, z0, z1) → U64(isNatKind(z1), z0, z1)
U64(tt, z0, z1) → s(plus(z1, z0))
isNat(0) → tt
isNat(plus(z0, z1)) → U11(isNatKind(z0), z0, z1)
isNat(s(z0)) → U21(isNatKind(z0), z0)
isNatKind(0) → tt
isNatKind(plus(z0, z1)) → U31(isNatKind(z0), z1)
isNatKind(s(z0)) → U41(isNatKind(z0))
plus(z0, 0) → U51(isNat(z0), z0)
plus(z0, s(z1)) → U61(isNat(z1), z1, z0)

Tuples:

U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
U51'(tt, z0) → c5(ISNATKIND(z0))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
U51'(tt, z0) → c5

S tuples:

U31'(tt, z0) → c9(ISNATKIND(z0))

K tuples:

U61'(tt, z0, z1) → c14(U62'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U62'(tt, z0, z1) → c15(U63'(isNat(z1), z0, z1), ISNAT(z1))
U63'(tt, z0, z1) → c16(U64'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U64'(tt, z0, z1) → c17(PLUS(z1, z0))
PLUS(z0, s(z1)) → c25(U61'(isNat(z1), z1, z0), ISNAT(z1))
PLUS(z0, 0) → c5(U51'(isNat(z0), z0))
PLUS(z0, 0) → c5(ISNAT(z0))
U51'(tt, z0) → c5
U51'(tt, z0) → c5(ISNATKIND(z0))
ISNAT(s(z0)) → c20(U21'(isNatKind(z0), z0), ISNATKIND(z0))
U21'(tt, z0) → c6(U22'(isNatKind(z0), z0), ISNATKIND(z0))
U22'(tt, z0) → c7(ISNAT(z0))
U11'(tt, z0, z1) → c(U12'(isNatKind(z0), z0, z1), ISNATKIND(z0))
ISNAT(plus(z0, z1)) → c19(U11'(isNatKind(z0), z0, z1), ISNATKIND(z0))
U12'(tt, z0, z1) → c1(U13'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U13'(tt, z0, z1) → c2(U14'(isNatKind(z1), z0, z1), ISNATKIND(z1))
U14'(tt, z0, z1) → c3(U15'(isNat(z0), z1), ISNAT(z0))
U15'(tt, z0) → c4(ISNAT(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))

Defined Rule Symbols:

U11, U12, U13, U14, U15, U16, U21, U22, U23, U31, U32, U41, U51, U52, U61, U62, U63, U64, isNat, isNatKind, plus

Defined Pair Symbols:

U11', U12', U13', U14', U21', U61', U62', U63', U64', ISNAT, ISNATKIND, PLUS, U51', U15', U22', U31'

Compound Symbols:

c, c1, c2, c3, c6, c14, c15, c16, c17, c19, c20, c22, c25, c5, c4, c7, c9, c23, c5

(23) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

U31'(tt, z0) → c9(ISNATKIND(z0))
ISNATKIND(plus(z0, z1)) → c22(U31'(isNatKind(z0), z1), ISNATKIND(z0))
ISNATKIND(s(z0)) → c23(ISNATKIND(z0))

Now S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(8) Obligation:

(9) CdtKnowledgeProof (EQUIVALENT transformation)

(10) Obligation:

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(12) Obligation:

(13) CdtKnowledgeProof (EQUIVALENT transformation)

(14) Obligation:

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(16) Obligation:

(17) CdtKnowledgeProof (EQUIVALENT transformation)

(18) Obligation:

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

(20) Obligation:

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

(22) Obligation:

(23) CdtKnowledgeProof (EQUIVALENT transformation)

(24) BOUNDS(O(1), O(1))